FDL - Nuprl Lemma : generated-thread-properties

Nuprl Lemma : generated-thread-properties

es:ES, P:(E

), R:(E

E

).
single-thread-generator{i:l}(es;P;R)

((

e, e':E. P(e)

P(e')

(((e R^+ e')

(e = e'))

(e' R^+ e)))

c

(

x, y:E. (P(x) & P(y))

((R^+(x,y))

(x < y)))

c

(

x, y:E. (R|P^+(x,y))

(R^+|P(x,y)))

c

(

x, y:E. (R|P(x,y))

(R|P^+!(x,y)))

c

(

x, y, x', y':E. (R|P^+(x,y))

(R|P(y',y))

((R|P^+(x,y'))

(x = y')))

c

(

x, y, x', y':E. (R|P^+(x,y))

(R|P(x',x))

(R|P(y',y))

(R|P^+(x',y'))))

Definitions R|P, sum_of_torder(T;R), A, Trans(T;x,y.E(x;y)), {T}, x:A. B(x), P Q, t T, P Q, P & Q, R^+, x f y, P Q, x(s), A c B, single-thread-generator{i:l}(es;P;R), P Q, , x:A. B(x), False, Dec(P), S T

Lemmas rel-immediate-preserves-order, rel-immediate-property, rel plus field, es-causl irreflexivity, rel plus trans, rel-is-immediate, rel plus-restriction-equiv, es-causle weakening, es-causl transitivity2, rel plus minimal, cond equiv to causl, es-causle wf, single-threaded-relation3, event system wf, not wf, rel implies wf, decidable wf, decidable es-E-equal, rel-immediate wf, rel plus wf, rel-restriction wf, es-causl wf, nat plus inc, rel exp wf, nat plus wf, es-E wf